bsort1(nil) -> nil
bsort1(.2(x, y)) -> last1(.2(bubble1(.2(x, y)), bsort1(butlast1(bubble1(.2(x, y))))))
bubble1(nil) -> nil
bubble1(.2(x, nil)) -> .2(x, nil)
bubble1(.2(x, .2(y, z))) -> if3(<=2(x, y), .2(y, bubble1(.2(x, z))), .2(x, bubble1(.2(y, z))))
last1(nil) -> 0
last1(.2(x, nil)) -> x
last1(.2(x, .2(y, z))) -> last1(.2(y, z))
butlast1(nil) -> nil
butlast1(.2(x, nil)) -> nil
butlast1(.2(x, .2(y, z))) -> .2(x, butlast1(.2(y, z)))
↳ QTRS
↳ DependencyPairsProof
bsort1(nil) -> nil
bsort1(.2(x, y)) -> last1(.2(bubble1(.2(x, y)), bsort1(butlast1(bubble1(.2(x, y))))))
bubble1(nil) -> nil
bubble1(.2(x, nil)) -> .2(x, nil)
bubble1(.2(x, .2(y, z))) -> if3(<=2(x, y), .2(y, bubble1(.2(x, z))), .2(x, bubble1(.2(y, z))))
last1(nil) -> 0
last1(.2(x, nil)) -> x
last1(.2(x, .2(y, z))) -> last1(.2(y, z))
butlast1(nil) -> nil
butlast1(.2(x, nil)) -> nil
butlast1(.2(x, .2(y, z))) -> .2(x, butlast1(.2(y, z)))
BUBBLE1(.2(x, .2(y, z))) -> BUBBLE1(.2(x, z))
BSORT1(.2(x, y)) -> BSORT1(butlast1(bubble1(.2(x, y))))
BSORT1(.2(x, y)) -> LAST1(.2(bubble1(.2(x, y)), bsort1(butlast1(bubble1(.2(x, y))))))
LAST1(.2(x, .2(y, z))) -> LAST1(.2(y, z))
BUTLAST1(.2(x, .2(y, z))) -> BUTLAST1(.2(y, z))
BSORT1(.2(x, y)) -> BUTLAST1(bubble1(.2(x, y)))
BUBBLE1(.2(x, .2(y, z))) -> BUBBLE1(.2(y, z))
BSORT1(.2(x, y)) -> BUBBLE1(.2(x, y))
bsort1(nil) -> nil
bsort1(.2(x, y)) -> last1(.2(bubble1(.2(x, y)), bsort1(butlast1(bubble1(.2(x, y))))))
bubble1(nil) -> nil
bubble1(.2(x, nil)) -> .2(x, nil)
bubble1(.2(x, .2(y, z))) -> if3(<=2(x, y), .2(y, bubble1(.2(x, z))), .2(x, bubble1(.2(y, z))))
last1(nil) -> 0
last1(.2(x, nil)) -> x
last1(.2(x, .2(y, z))) -> last1(.2(y, z))
butlast1(nil) -> nil
butlast1(.2(x, nil)) -> nil
butlast1(.2(x, .2(y, z))) -> .2(x, butlast1(.2(y, z)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
BUBBLE1(.2(x, .2(y, z))) -> BUBBLE1(.2(x, z))
BSORT1(.2(x, y)) -> BSORT1(butlast1(bubble1(.2(x, y))))
BSORT1(.2(x, y)) -> LAST1(.2(bubble1(.2(x, y)), bsort1(butlast1(bubble1(.2(x, y))))))
LAST1(.2(x, .2(y, z))) -> LAST1(.2(y, z))
BUTLAST1(.2(x, .2(y, z))) -> BUTLAST1(.2(y, z))
BSORT1(.2(x, y)) -> BUTLAST1(bubble1(.2(x, y)))
BUBBLE1(.2(x, .2(y, z))) -> BUBBLE1(.2(y, z))
BSORT1(.2(x, y)) -> BUBBLE1(.2(x, y))
bsort1(nil) -> nil
bsort1(.2(x, y)) -> last1(.2(bubble1(.2(x, y)), bsort1(butlast1(bubble1(.2(x, y))))))
bubble1(nil) -> nil
bubble1(.2(x, nil)) -> .2(x, nil)
bubble1(.2(x, .2(y, z))) -> if3(<=2(x, y), .2(y, bubble1(.2(x, z))), .2(x, bubble1(.2(y, z))))
last1(nil) -> 0
last1(.2(x, nil)) -> x
last1(.2(x, .2(y, z))) -> last1(.2(y, z))
butlast1(nil) -> nil
butlast1(.2(x, nil)) -> nil
butlast1(.2(x, .2(y, z))) -> .2(x, butlast1(.2(y, z)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
BUTLAST1(.2(x, .2(y, z))) -> BUTLAST1(.2(y, z))
bsort1(nil) -> nil
bsort1(.2(x, y)) -> last1(.2(bubble1(.2(x, y)), bsort1(butlast1(bubble1(.2(x, y))))))
bubble1(nil) -> nil
bubble1(.2(x, nil)) -> .2(x, nil)
bubble1(.2(x, .2(y, z))) -> if3(<=2(x, y), .2(y, bubble1(.2(x, z))), .2(x, bubble1(.2(y, z))))
last1(nil) -> 0
last1(.2(x, nil)) -> x
last1(.2(x, .2(y, z))) -> last1(.2(y, z))
butlast1(nil) -> nil
butlast1(.2(x, nil)) -> nil
butlast1(.2(x, .2(y, z))) -> .2(x, butlast1(.2(y, z)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
BUTLAST1(.2(x, .2(y, z))) -> BUTLAST1(.2(y, z))
POL(.2(x1, x2)) = 1 + x2
POL(BUTLAST1(x1)) = 1 + x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
bsort1(nil) -> nil
bsort1(.2(x, y)) -> last1(.2(bubble1(.2(x, y)), bsort1(butlast1(bubble1(.2(x, y))))))
bubble1(nil) -> nil
bubble1(.2(x, nil)) -> .2(x, nil)
bubble1(.2(x, .2(y, z))) -> if3(<=2(x, y), .2(y, bubble1(.2(x, z))), .2(x, bubble1(.2(y, z))))
last1(nil) -> 0
last1(.2(x, nil)) -> x
last1(.2(x, .2(y, z))) -> last1(.2(y, z))
butlast1(nil) -> nil
butlast1(.2(x, nil)) -> nil
butlast1(.2(x, .2(y, z))) -> .2(x, butlast1(.2(y, z)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
LAST1(.2(x, .2(y, z))) -> LAST1(.2(y, z))
bsort1(nil) -> nil
bsort1(.2(x, y)) -> last1(.2(bubble1(.2(x, y)), bsort1(butlast1(bubble1(.2(x, y))))))
bubble1(nil) -> nil
bubble1(.2(x, nil)) -> .2(x, nil)
bubble1(.2(x, .2(y, z))) -> if3(<=2(x, y), .2(y, bubble1(.2(x, z))), .2(x, bubble1(.2(y, z))))
last1(nil) -> 0
last1(.2(x, nil)) -> x
last1(.2(x, .2(y, z))) -> last1(.2(y, z))
butlast1(nil) -> nil
butlast1(.2(x, nil)) -> nil
butlast1(.2(x, .2(y, z))) -> .2(x, butlast1(.2(y, z)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
LAST1(.2(x, .2(y, z))) -> LAST1(.2(y, z))
POL(.2(x1, x2)) = 1 + x2
POL(LAST1(x1)) = 1 + x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
bsort1(nil) -> nil
bsort1(.2(x, y)) -> last1(.2(bubble1(.2(x, y)), bsort1(butlast1(bubble1(.2(x, y))))))
bubble1(nil) -> nil
bubble1(.2(x, nil)) -> .2(x, nil)
bubble1(.2(x, .2(y, z))) -> if3(<=2(x, y), .2(y, bubble1(.2(x, z))), .2(x, bubble1(.2(y, z))))
last1(nil) -> 0
last1(.2(x, nil)) -> x
last1(.2(x, .2(y, z))) -> last1(.2(y, z))
butlast1(nil) -> nil
butlast1(.2(x, nil)) -> nil
butlast1(.2(x, .2(y, z))) -> .2(x, butlast1(.2(y, z)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
BUBBLE1(.2(x, .2(y, z))) -> BUBBLE1(.2(x, z))
BUBBLE1(.2(x, .2(y, z))) -> BUBBLE1(.2(y, z))
bsort1(nil) -> nil
bsort1(.2(x, y)) -> last1(.2(bubble1(.2(x, y)), bsort1(butlast1(bubble1(.2(x, y))))))
bubble1(nil) -> nil
bubble1(.2(x, nil)) -> .2(x, nil)
bubble1(.2(x, .2(y, z))) -> if3(<=2(x, y), .2(y, bubble1(.2(x, z))), .2(x, bubble1(.2(y, z))))
last1(nil) -> 0
last1(.2(x, nil)) -> x
last1(.2(x, .2(y, z))) -> last1(.2(y, z))
butlast1(nil) -> nil
butlast1(.2(x, nil)) -> nil
butlast1(.2(x, .2(y, z))) -> .2(x, butlast1(.2(y, z)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
BUBBLE1(.2(x, .2(y, z))) -> BUBBLE1(.2(x, z))
BUBBLE1(.2(x, .2(y, z))) -> BUBBLE1(.2(y, z))
POL(.2(x1, x2)) = 1 + x2
POL(BUBBLE1(x1)) = 1 + x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
bsort1(nil) -> nil
bsort1(.2(x, y)) -> last1(.2(bubble1(.2(x, y)), bsort1(butlast1(bubble1(.2(x, y))))))
bubble1(nil) -> nil
bubble1(.2(x, nil)) -> .2(x, nil)
bubble1(.2(x, .2(y, z))) -> if3(<=2(x, y), .2(y, bubble1(.2(x, z))), .2(x, bubble1(.2(y, z))))
last1(nil) -> 0
last1(.2(x, nil)) -> x
last1(.2(x, .2(y, z))) -> last1(.2(y, z))
butlast1(nil) -> nil
butlast1(.2(x, nil)) -> nil
butlast1(.2(x, .2(y, z))) -> .2(x, butlast1(.2(y, z)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
BSORT1(.2(x, y)) -> BSORT1(butlast1(bubble1(.2(x, y))))
bsort1(nil) -> nil
bsort1(.2(x, y)) -> last1(.2(bubble1(.2(x, y)), bsort1(butlast1(bubble1(.2(x, y))))))
bubble1(nil) -> nil
bubble1(.2(x, nil)) -> .2(x, nil)
bubble1(.2(x, .2(y, z))) -> if3(<=2(x, y), .2(y, bubble1(.2(x, z))), .2(x, bubble1(.2(y, z))))
last1(nil) -> 0
last1(.2(x, nil)) -> x
last1(.2(x, .2(y, z))) -> last1(.2(y, z))
butlast1(nil) -> nil
butlast1(.2(x, nil)) -> nil
butlast1(.2(x, .2(y, z))) -> .2(x, butlast1(.2(y, z)))